CS259 Mobile IPv6 Binding Updates - Return Routability Procedure
Murphi Simulation Code Manual
Andre Encarnacao
Greg Bayer
March 2008

Code Contents:
- There are five project folders included, each titled "project_i" for i=1 to 5.
- Folders correspond to project versions that we used in our rational reconstruction
of the protocol. Please refer to our final project report to see specific details on
each version of the protocol.
- Each folder contains two files: proji.m and Makefile

How to run the code using Murphi:
- The *.m file contains the Murphi model of that particular reconstruction version
of the protocol. To get an executable verifier, just type "make". Murphi will
produce the C++ code of the verifier which will then be compiled into an 
executable called "proji".
- You can run the Murphi verifier by "proji -ndl -tv". The first option "-ndl" 
disables the checking for deadlock states, and the second option "-tv" writes
a violating trace (if one is found).

Murphi documentation:
- Please refer to the following website for general information (including how
to install and use Murphi): http://verify.stanford.edu/dill/murphi.html
- Please refer to the following website for a Reference Manual on using Murphi:
http://chicory.stanford.edu/dill/Murphi/Murphi3.1/doc/User.Manual
